                  PointerC-x86
=================================================================

1. Things to note
  + Here, we only list the non-code part of the lexical and syntactic
    rules.
  + Do NOT touch the data section now.

2. Lexical rules
  + Every non-code part starts with "#@", ends with "#@"
  + Reserved key words are symbols quoted by "", see the following
    production rules for details.
    
3. Syntax
  + * denotes zeor or more repetion
  + // denotes meta-level comments
  
prog      ::= typeDec fun-rettype-dec textSec dataSec

typeDec   ::= "struct" sid
              "{"
                 intNum ":" type ";" *
              "}" *     // cliu, one or more?

fun-rettype-dec ::= "id" ":" type ";" +

textSec   ::= function *

function  ::= varDec prePost

varDec    ::= type aptr "," aptr ";" *

prePost   ::= "pre" "=" pprop 
              "post" "=" pprop
// see "src/asm/assem.sig" for details          
type      ::= "int"
           |  type*
           |  "struct" id
           |  "wild" 

// see "src/asm/assem.sig" for details
pprop     ::= "true"
           |  pprop "&&" pprop
           |  pprop "||" pprop
           |  pprop "->" pprop
           |  "!"pprop
           |  "(" "{" aptr ("," aptr)+ "}" ")"
           |  "{" aptr ("," aptr)+ "}""N"
           |  "{" aptr ("," aptr)+ "}""D"
           |  "forall" id":"type"." pprop
           |  "exists" id":"type"." pprop
           |  "tree" "(" pexp ")"
           |  "list" "(" pexp ")"
           |  pexp ">" pexp
           |  pexp ">=" pexp
           |  pexp "<" pexp
           |  pexp "<=" pexp
           |  pexp "==" pexp
           |  pexp "!=" pexp
           |  id "(" pprop ")"

pexp      ::= aptr
           |  intNum
           |  pexp "+" pexp
           |  pexp "-" pexp
           |  pexp "*" pexp
           |  "(" pexp ")"

aptr      ::= reg
           |  intNum"("reg")"
           |  intNum"("reg")""(""->"intNum")"pexp
           |  id
4. Example
The following is peseudocode example, to illustrate various rules.
******************************************************************

#@ struct list
#  {
#    0 : int           ;
#    4 : struct list * ;
#  }
#@
	.text
	.align 4

#@ int* 8(%ebp),  -4(%esp);
#  int -4(%ebp),  -8(%esp);
#  int* 12(%ebp), -12(%esp);
#@

#@ pre = ({8(%ebp)}) /\ {12(%ebp)}N
#  post = true
#@
	.globl f
f: 
#@ true
#@
	pushl	%ebp
	movl	%esp, %ebp
	...
	jmp .L

        ...

	ret





#@ int 8(%ebp);
#  int -4(%ebp);
#  int* 12(%ebp);
#@

#@ pre = {12(%ebp)}N
#  post = true
#@
	.globl g
f: 
#@ true
#@
	pushl	%ebp
	movl	%esp, %ebp
	...
	jmp .L

        ...

	ret
	